Runtime Complexity (full) proof of /tmp/tmphOPU9Q/sat.xml

The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

0 CpxTRS

↳1 DecreasingLoopProof (⇔, 491 ms)

↳2 BOUNDS(n^1, INF)

↳3 RenamingProof (⇔, 0 ms)

↳4 CpxRelTRS

    ↳5 SlicingProof (LOWER BOUND(ID), 0 ms)

    ↳6 CpxRelTRS

    ↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 typed CpxTrs

    ↳9 OrderProof (LOWER BOUND(ID), 0 ms)

    ↳10 typed CpxTrs

    ↳11 NoRewriteLemmaProof (LOWER BOUND(ID), 25 ms)

    ↳12 typed CpxTrs

    ↳13 RewriteLemmaProof (LOWER BOUND(ID), 1025 ms)

    ↳14 BEST

        ↳15 typed CpxTrs

            ↳16 RewriteLemmaProof (LOWER BOUND(ID), 42 ms)

            ↳17 BEST

                ↳18 typed CpxTrs

                    ↳19 RewriteLemmaProof (LOWER BOUND(ID), 240 ms)

                    ↳20 BEST

                        ↳21 typed CpxTrs

                            ↳22 NoRewriteLemmaProof (LOWER BOUND(ID), 746 ms)

                            ↳23 typed CpxTrs

                            ↳24 LowerBoundsProof (⇔, 0 ms)

                            ↳25 BOUNDS(n^1, INF)

                        ↳26 typed CpxTrs

                            ↳27 LowerBoundsProof (⇔, 0 ms)

                            ↳28 BOUNDS(n^1, INF)

                ↳29 typed CpxTrs

                    ↳30 LowerBoundsProof (⇔, 0 ms)

                    ↳31 BOUNDS(n^1, INF)

        ↳32 typed CpxTrs

            ↳33 LowerBoundsProof (⇔, 0 ms)

            ↳34 BOUNDS(n^1, INF)

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
member(x, cons(y, ys)) →⁺ if(eq(x, y), true, member(x, ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: FULL

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
satck/0

(6) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: FULL

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

TRS:
Rules:
if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(guess(cnf))
satck(assign) → if(verify(assign), assign, unsat)

Types:
if :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
true :: true:false:nil:cons:O:0:1:unsat
false :: true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
nil :: true:false:nil:cons:O:0:1:unsat
cons :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
eq :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
O :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
1 :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
negate :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
guess :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat → true:false:nil:cons:O:0:1:unsat
unsat :: true:false:nil:cons:O:0:1:unsat
hole_true:false:nil:cons:O:0:1:unsat1_2 :: true:false:nil:cons:O:0:1:unsat
gen_true:false:nil:cons:O:0:1:unsat2_2 :: Nat → true:false:nil:cons:O:0:1:unsat

(9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
member, eq, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(10) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
eq, member, choice, guess, verify

They will be analysed ascendingly in the following order:
eq < member
member < verify
choice < guess

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol eq.

(12) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
member, choice, guess, verify

They will be analysed ascendingly in the following order:
member < verify
choice < guess

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Induction Base:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n127_2, 1)))) →_R^Ω(1)
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2)))) →_IH
if(eq(gen_true:false:nil:cons:O:0:1:unsat2_2(a), true), true, *3_2)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
choice, guess, verify

They will be analysed ascendingly in the following order:
choice < guess

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n131688₂)

Induction Base:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n131688_2, 1)))) →_R^Ω(1)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) →_IH
*3_2

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)
choice(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n131688_2))) → *3_2, rt ∈ Ω(n131688₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
guess, verify

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2))) → *3_2, rt ∈ Ω(n132159₂)

Induction Base:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, 0)))

Induction Step:
guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, +(n132159_2, 1)))) →_R^Ω(1)
cons(choice(true), guess(gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n132159_2)))) →_IH
cons(choice(true), *3_2)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(20) Complex Obligation (BEST)

(21) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

The following defined symbols remain to be analysed:
verify

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol verify.

(23) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(25) BOUNDS(n^1, INF)

(26) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat2_2(0) ⇔ true
gen_true:false:nil:cons:O:0:1:unsat2_2(+(x, 1)) ⇔ cons(true, gen_true:false:nil:cons:O:0:1:unsat2_2(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
member(gen_true:false:nil:cons:O:0:1:unsat2_2(a), gen_true:false:nil:cons:O:0:1:unsat2_2(+(1, n127_2))) → *3_2, rt ∈ Ω(n127₂)

(0) Obligation:

(1) DecreasingLoopProof (EQUIVALENT transformation)

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

(4) Obligation:

(5) SlicingProof (LOWER BOUND(ID) transformation)

(6) Obligation:

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) OrderProof (LOWER BOUND(ID) transformation)

(10) Obligation:

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(12) Obligation:

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(14) Complex Obligation (BEST)

(15) Obligation:

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(17) Complex Obligation (BEST)

(18) Obligation:

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

(20) Complex Obligation (BEST)

(21) Obligation:

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

(23) Obligation:

(24) LowerBoundsProof (EQUIVALENT transformation)

(25) BOUNDS(n^1, INF)

(26) Obligation:

(27) LowerBoundsProof (EQUIVALENT transformation)

(28) BOUNDS(n^1, INF)

(29) Obligation:

(30) LowerBoundsProof (EQUIVALENT transformation)

(31) BOUNDS(n^1, INF)

(32) Obligation:

(33) LowerBoundsProof (EQUIVALENT transformation)

(34) BOUNDS(n^1, INF)